*****LABEL I_RID;

*****∧I LISTINDUCTION1;

1 ((qNIL*qNIL)=qNIL∧∀uu.((cdr uu*qNIL)=cdr uu⊃(uu*qNIL)=uu))⊃∀u.(u*qNIL)=u  

*****LABEL NIL_RID;

*****EVAL qNIL*qNIL BY { APPEND_DEF};

2 (qNIL*qNIL)=qNIL  

*****LABEL H_RID;

*****ASSUME (cdr uu*qNIL)=cdr uu;

3 (cdr uu*qNIL)=cdr uu  (3)

*****REWRITE uu*qNIL BY LOGICTREE∪SEXPSS∪{ APPEND_DEF,H_RID};

4 (uu*qNIL)=uu  (3)

*****⊃I H_RID⊃↑;

5 (cdr uu*qNIL)=cdr uu⊃(uu*qNIL)=uu  

*****∀I ↑ uu;

6 ∀uu.((cdr uu*qNIL)=cdr uu⊃(uu*qNIL)=uu)  

*****TAUT ∀u.(u*qNIL)=u I_RID:NIL_RID,6;

7 ∀u.(u*qNIL)=u  

*****LABEL I_ASS;

*****∧I LISTINDUCTION1;

8 (∀v w.(qNIL*(v*w))=((qNIL*v)*w)∧∀uu.(∀v w.(cdr uu*(v*w))=((cdr uu*v)*w)⊃∀v w.(uu*(v*w))=((uu*v)*w)))⊃∀u v w.(u%
*(v*w))=((u*v)*w)  

*****LABEL NIL_ASS;

*****EVAL ∀v w.(qNIL*(v*w))=((qNIL*v)*w) BY { APPEND_DEF};

9 ∀v w.(qNIL*(v*w))=((qNIL*v)*w)  

*****LABEL H_ASS;

*****ASSUME ∀v w.(cdr uu*(v*w))=((cdr uu*v)*w);

10 ∀v w.(cdr uu*(v*w))=((cdr uu*v)*w)  (10)

*****REWRITE ∀v w.(uu*(v*w))=((uu*v)*w) BY LOGICTREE∪SEXPSS∪{ APPEND_DEF,H_ASS};

11 ∀v w.(uu*(v*w))=((uu*v)*w)  (10)

*****⊃I H_ASS⊃↑;

12 ∀v w.(cdr uu*(v*w))=((cdr uu*v)*w)⊃∀v w.(uu*(v*w))=((uu*v)*w)  

*****∀I ↑ uu;

13 ∀uu.(∀v w.(cdr uu*(v*w))=((cdr uu*v)*w)⊃∀v w.(uu*(v*w))=((uu*v)*w))  

*****TAUT ∀u v w.(u*(v*w))=((u*v)*w) I_ASS:NIL_ASS,13;

14 ∀u v w.(u*(v*w))=((u*v)*w)  

*****LABEL I_DIS;

*****∧I LISTINDUCTION1;

15 (∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w))∧∀uu.(∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)%
=rev1(v,rev1(uu,w))))⊃∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w))  

*****LABEL NIL_DIS;

*****EVAL ∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w)) BY { APPEND_DEF,REV1_DEF};

16 ∀v w.rev1(qNIL*v,w)=rev1(v,rev1(qNIL,w))  

*****LABEL H_DIS;

*****ASSUME ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w));

17 ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))  (17)

*****∀E APPEND_DEF uu,v;

18 (uu*v)=IF NULL uu THEN v ELSE cons(car uu,cdr uu*v)  

*****REWRITE ∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w)) BY LOGICTREE∪SEXPSS∪{ REV1_DEF,H_DIS:18};

19 ∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w))  (17)

*****⊃I H_DIS⊃↑;

20 ∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w))  

*****∀I ↑ uu;

21 ∀uu.(∀v w.rev1(cdr uu*v,w)=rev1(v,rev1(cdr uu,w))⊃∀v w.rev1(uu*v,w)=rev1(v,rev1(uu,w)))  

*****TAUT ∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w)) I_DIS:NIL_DIS,21;

22 ∀u v w.rev1(u*v,w)=rev1(v,rev1(u,w))